import {Formula} from './formula.js'
import {isSubtypeOf, type Type} from './type.js'
import {
    type Term, type VariableSpecification,
    FreeVariableTerm, FunctionTerm, QuantifiedVariableTerm,
} from './term.js'
import {
    type PredicateSpecification,
    stringify as stringifyPredicateSpecification,
    areEqual as arePredicateSpecificationsEqual,
} from './predicateSpecification.js'
import {
    stringify as stringifyFunctionSpecification,
    areEqual as areFunctionSpecificationsEqual,
    type FunctionSpecification,
} from './functionSpecification.js'
import {pipe, map, take, zip, includes, every, forEach, flat, tap, reverse, toArray, filter} from './iterator.js'
import {Tokenizer, getLineDataFromIndex, type Token, type TokenType} from './tokenizer.js'
import {Verifier} from './verifier.js'
import {Reasoner} from './reasoner.js'
import {createObjectMap} from './utils/createObjectMap.js'

const symbolStopTokens: readonly TokenType[] = ['_space_', '_comment_', ',', ';', '_eof_']

export class ClassSyntaxError {
    constructor(public message: string, public token: Token) {}
}

type SymbolInfo =
    | {kind: 'relation'}
    | {kind: 'operation', precedence: number}
    | {kind: 'leftBracket', pair: string}
    | {kind: 'rightBracket'}

export class Parser {
    text: string
    tokens: Tokenizer
    token: Token
    peekedToken: Token | undefined
    previousToken: Token = {
        index: 0,
        type: 'environ',
        string: '',
    }

    symbols = createObjectMap<string, SymbolInfo | undefined>()
    predicateSpecifications = createObjectMap<string, PredicateSpecification[] | undefined>()
    functionSpecifications = createObjectMap<string, FunctionSpecification[] | undefined>()
    sparseOperationPrecedences: (string[] | undefined)[] = []
    operationPrecedences: string[][] = []

    verifier: Verifier
    reasoner: Reasoner

    logger?: (message: string, token?: Token) => void

    constructor(text: string) {
        this.text = text
        this.tokens = new Tokenizer(text)

        this.reasoner = new Reasoner
        this.verifier = new Verifier

        this.token = this.nextToken()
    }

    setErrorLogger(logger: typeof this.logError) {
        this.logger = logger
    }

    logError(message: string, token = this.previousToken) {
        if (this.logger) {
            this.logger(message, token)
            return
        }

        const {offset, line, lineNumber} = getLineDataFromIndex(token.index, this.text)

        console.error(`error in line ${lineNumber}:`)
        console.error(line)
        console.error(`${' '.repeat(offset)}^`, message)
    }

    error(message: string, token = this.previousToken) {
        return new ClassSyntaxError(message, token)
    }

    addProposition({label, formula}: {label: number, formula: Formula}) {
        this.verifier.addFormula(label, formula)
    }

    parse() {
        try {
            this.parseArticle()
        } catch (error) {
            if (error instanceof ClassSyntaxError)
                this.logError(error.message, error.token)
            else
                throw error
        }
    }

    parseArticle() {
        loop:
        for (;;)
            switch (this.token.type) {
            case 'environ':
                this.parseEnviron()
                break
            case 'text':
                this.parseText()
                break
            case '_eof_':
                break loop
            default:
                throw this.error('syntax error', this.token)
            }
    }

    parseEnviron() {
        this.consumeToken('environ')

        for (;;)
            switch (this.token.type) {
            case 'relations':
                this.parseRelations()
                break
            case 'operations':
                this.parseOperations()
                break
            case 'brackets':
                this.parseBrackets()
                break
            case 'type':
                this.parseTypeSpecification()
                break
            case 'reserve':
                this.parseReservation()
                break
            case 'pred':
                this.parsePredicateSpecification()
                break
            case 'func':
            case 'constructor':
                this.parseFunctionSpecification()
                break
            case 'environ':
            case 'text':
            case '_eof_':
                return
            default:
                this.addProposition(this.parseProposition())
                this.consumeToken(';')
            }
    }

    parseText() {
        this.consumeToken('text')

        for (;;)
            switch (this.token.type) {
            case 'reserve':
                this.parseReservation()
                break
            case 'begin':
                this.parseBegin()
                break
            case 'environ':
            case 'text':
            case '_eof_':
                return
            default:
                this.parseStatement()
                break
            }
    }

    maybeParseLabel() {
        let label = +this.token.string

        if (this.tryConsumeToken('_number_'))
            this.consumeToken(':')
        else
            label = -1

        return label
    }

    parseStatement() {
        const label = this.maybeParseLabel()

        return this.token.type === 'begin'
            ? this.parseBegin(label)
            : this.parseCompactStatement(label)
    }

    parseCompactStatement(label = -1) {
        const formulaToken = this.token
        const formula = this.parseFormula()

        if (this.token.type === 'proof')
            this.parseProof(formula)
        else {
            if (this.tryConsumeToken('by'))
                pipe(this.parseList(this.parseLabel), forEach())

            if (!this.verifier.verify(formula))
                this.logError('inference not accepted', this.token)
        }

        this.verifier.addFormula(label, formula)
        this.consumeToken(';')

        return {formula, formulaToken}
    }

    parseProof(formula: Formula) {
        this.consumeToken('proof')

        const oldReasoner = this.reasoner
        const oldVerifier = this.verifier
        this.reasoner = new Reasoner(formula)
        this.verifier = new Verifier(this.verifier)

        this.parseReasoning()
        this.consumeToken('qed')

        if (this.reasoner.thesis !== Formula.True)
            this.logError('proof structure does not match thesis')

        this.verifier = oldVerifier
        this.reasoner = oldReasoner
    }

    parseBegin(label = -1) {
        this.consumeToken('begin')

        const oldReasoner = this.reasoner
        const oldVerifier = this.verifier
        this.reasoner = new Reasoner
        this.verifier = new Verifier(this.verifier)

        this.parseReasoning()
        this.consumeToken('end')
        this.consumeToken(';')

        const thesis = this.reasoner.getReasoningThesis()

        this.verifier = oldVerifier
        this.reasoner = oldReasoner

        this.verifier.addFormula(label, thesis)
    }

    parseReasoning() {
        loop:
        for (;;)
            switch (this.token.type) {
            case 'let':
                this.nextToken()
                this.verifier.clearLastFormula()
                this.parseLet()
                break

            case 'given':
                this.nextToken()
                this.verifier.clearLastFormula()
                this.parseGiven()
                break

            case 'consider':
                this.nextToken()
                this.verifier.clearLastFormula()
                this.parseConsider()
                break

            case 'take':
                this.nextToken()
                this.verifier.clearLastFormula()
                this.parseTake()
                break

            case 'assume':
                this.nextToken()
                this.parseAssume()
                break

            case 'then':
                if (!this.verifier.referenceLastFormula())
                    this.logError('invalid "then" usage', this.token)

                this.nextToken()
                this.parseThenStatement()
                break

            case 'hence':
                if (!this.verifier.referenceLastFormula())
                    this.logError('invalid "hence" usage', this.token)
                // fall through

            case 'thus':
                this.nextToken()
                this.parseThus()
                break

            case 'qed':
            case 'end':
                break loop

            default:
                this.parseStatement()
            }
    }

    parseLet() {
        pipe(
            this.parseList(this.parseQualifiedVariable),
            map(varSpec => new FreeVariableTerm(varSpec)),
            forEach(variable => {
                this.verifier.addFreeVariable(variable)
                this.reasoner.checkLet(variable) || this.logError('generalization disagrees with thesis')
            }),
        )

        if (this.tryConsumeToken('such')) {
            this.consumeToken('that')
            this.parseAssume()
        } else
            this.consumeToken(';')
    }

    parseGiven() {
        pipe(
            this.parseList(this.parseQualifiedVariable),
            map(varSpec => new FreeVariableTerm(varSpec)),
            forEach(variable => {
                this.verifier.addFreeVariable(variable)
                this.reasoner.checkGiven(variable) || this.logError('existential assumption disagrees with thesis')
            }),
        )

        if (this.tryConsumeToken('such')) {
            this.consumeToken('that')
            this.parseAssume()
        } else
            this.consumeToken(';')
    }

    parseConsider() {
        const variables = pipe(
            this.parseList(this.parseQualifiedVariable),
            map(varSpec => new FreeVariableTerm(varSpec)),
            tap(variable => this.verifier.addFreeVariable(variable)),
            toArray,
        )

        const clauses: Formula[] = []

        if (this.tryConsumeToken('such')) {
            this.consumeToken('that')

            clauses.push(...pipe(
                this.parseList(this.parseProposition, 'and'),
                tap(proposition => this.addProposition(proposition)),
                map(proposition => proposition.formula),
            ))

            if (this.tryConsumeToken('by'))
                pipe(this.parseList(this.parseLabel), forEach())
        }

        if (!this.verifier.verifyConsider(variables, clauses))
            this.logError('choice not accepted')

        this.consumeToken(';')
    }

    parseTake() {
        pipe(
            this.parseList(this.parseQualifiedVariable),
            map(varSpec => new FreeVariableTerm(varSpec)),
            forEach(variable => {
                this.verifier.addFreeVariable(variable)
                this.reasoner.checkTake(variable) || this.logError('exemplification disagrees with thesis')
            }),
        )

        this.consumeToken(';')
    }

    parseAssume() {
        pipe(
            this.parseList(this.parseProposition, 'and'),
            forEach(proposition => {
                this.addProposition(proposition)

                if (!this.reasoner.checkAssume(proposition.formula))
                    this.logError('assumption disagrees with thesis', proposition.formulaToken)
            }),
        )

        this.consumeToken(';')
    }

    parseThenStatement() {
        return this.tryConsumeToken('consider')
            ? this.parseConsider()
            : this.parseCompactStatement(this.maybeParseLabel())
    }

    parseThus() {
        const {formula, formulaToken} = this.parseCompactStatement(this.maybeParseLabel())

        if (!this.reasoner.checkThus(formula))
            this.logError('conclusion disagrees with thesis', formulaToken)
    }

    parseLabel() {
        const {token} = this

        if (!this.tryConsumeToken('_number_'))
            throw this.error(`label expected but "${token.string}" found`, token)

        const label = +token.string

        if (!this.verifier.referenceFormulaByLabel(label))
            this.logError(`label "${label}" not found`, token)

        return {label, token}
    }

    parseRelations() {
        this.consumeToken('relations')

        for (const symbol of this.parseList(this.parseSymbol))
            this.addSymbol(symbol, {kind: 'relation'})

        this.consumeToken(';')
    }

    * parseList<T>(elementParser: (this: Parser) => T, delimiterToken: TokenType = ',') {
        for (;;) {
            yield elementParser.call(this)
            if (!this.tryConsumeToken(delimiterToken))
                break
        }
    }

    parseSymbol() {
        let name = ''

        while (!symbolStopTokens.includes(this.token.type)) {
            name += this.token.string
            this.nextLooseToken()
        }

        if (['_space_', '_comment_'].includes(this.token.type))
            this.nextToken()

        return name
    }

    parseOperations() {
        this.consumeToken('operations')

        forEach()(this.parseList(this.parseOperationSegment))

        this.operationPrecedences = [...pipe(this.sparseOperationPrecedences, filter(Boolean))]
    }

    parseOperationSegment() {
        for (;;) {
            const symbols = [...this.parseList(this.parseSymbol)]
            let precedence = 0

            if (this.tryConsumeToken('precedence')) {
                precedence = +this.token.string

                this.consumeToken('_number_')

                if (precedence < 1 || precedence > 255) {
                    this.logError('precedence must be 1..255')
                    precedence = 0
                }
            }

            precedence ||= 64

            for (const symbol of symbols) {
                this.addSymbol(symbol, {
                    kind: 'operation',
                    precedence,
                });

                (this.sparseOperationPrecedences[precedence] ||= []).push(symbol)
            }

            if (!this.tryConsumeToken(','))
                break
        }

        this.nextToken()
    }

    parseBrackets() {
        this.consumeToken('brackets')

        for (const [symbol1, symbol2] of this.parseList(this.parseBracketPair)) {
            this.addSymbol(symbol1, {
                kind: 'leftBracket',
                pair: symbol2,
            })
            this.addSymbol(symbol2, {kind: 'rightBracket'})
        }

        this.consumeToken(';')
    }

    parseBracketPair(): [string, string] {
        return [this.parseSymbol(), this.parseSymbol()]
    }

    parseTypeSpecification() {
        this.consumeToken('type')

        const nameToken = this.token
        const name = this.parseIdentifier()

        const baseTypes: Type[] = []

        if (this.tryConsumeToken('->'))
            baseTypes.push(...this.parseList(this.parseType))

        if (!this.verifier.addType(name, baseTypes))
            this.logError(`duplicate type "${name}"`, nameToken)

        this.consumeToken(';')
    }

    parseType() {
        const name = this.parseIdentifier()
        const type = this.verifier.types[name]

        if (!type) {
            this.logError(`unknown type "${name}"`)
            return Verifier.defaultType
        }

        return type
    }

    parseReservation() {
        this.consumeToken('reserve')

        forEach()(this.parseList(this.parseReservationSegment))
        this.consumeToken(';')
    }

    parseReservationSegment() {
        const names = [...this.parseList(this.parseIdentifier)]

        this.consumeToken('for')

        const type = this.parseType()

        for (const name of names)
            this.verifier.reserve(name, type)
    }

    parseIdentifier() {
        const name = this.token.string
        this.consumeToken('_identifier_')
        return name
    }

    parsePredicateSpecification() {
        this.consumeToken('pred')

        const parameters = this.symbols[this.token.string]?.kind === 'relation'
            ? []
            : [...this.parseList(this.parseType)]
        const symbolOffset = parameters.length
        const name = this.token.string
        const symbolToken = this.token

        this.consumeToken('_symbol_')

        if (this.token.type !== ';')
            pipe(
                this.parseList(this.parseType),
                forEach(type => parameters.push(type)),
            )

        const newSpecification = {
            name,
            symbolOffset,
            parameterTypes: parameters,
        }
        const specifications = this.predicateSpecifications[name] ||= []

        if (specifications.some(specification => arePredicateSpecificationsEqual(specification, newSpecification)))
            this.logError(
                `duplicate predicate specification "${stringifyPredicateSpecification(newSpecification)}"`,
                symbolToken,
            )
        else
            specifications.push(newSpecification)

        this.consumeToken(';')
    }

    parseFunctionSpecification() {
        const isConstructor = this.tryConsumeToken('constructor')

        if (!isConstructor)
            this.consumeToken('func')

        const symbol = this.symbols[this.token.string]
        const functionPattern = symbol?.kind === 'leftBracket'
            ? this.parseBracketPattern(symbol)
            : this.parseOperationPattern()

        const symbolToken = this.token

        this.consumeToken('->')

        const newSpecification = {
            ...functionPattern,
            type: this.parseType(),
        }
        const functionName = 'name' in newSpecification ? newSpecification.name : newSpecification.left

        const specifications = this.functionSpecifications[functionName] ||= []

        if (specifications.some(specification => areFunctionSpecificationsEqual(specification, newSpecification)))
            this.logError(
                `duplicate function specification "${stringifyFunctionSpecification(newSpecification)}"`,
                symbolToken,
            )
        else
            specifications.push(newSpecification)

        this.consumeToken(';')
    }

    parseOperationPattern() {
        const parameters = this.symbols[this.token.string]?.kind === 'operation'
            ? []
            : [...this.parseList(this.parseType)]
        const symbolOffset = parameters.length
        const name = this.token.string

        if (this.symbols[name]?.kind !== 'operation')
            throw this.error(`operation symbol expected but "${name}" found`, this.token)

        this.nextToken()

        if (this.token.type !== '->')
            parameters.push(...this.parseList(this.parseType))

        return {
            name,
            symbolOffset,
            parameterTypes: parameters,
        }
    }

    parseBracketPattern(symbol: {pair: string}) {
        const left = this.token.string
        const right = symbol.pair

        this.nextToken()

        const parameters = this.token.string === right
            ? []
            : [...this.parseList(this.parseType)]

        if (this.token.string !== right)
            throw this.error(`closing bracket "${right}" expected but "${this.token.string}" found`, this.token)

        this.nextToken()

        return {
            left,
            right,
            parameterTypes: parameters,
        }
    }

    parseProposition() {
        return {
            label: this.maybeParseLabel(),
            formulaToken: this.token,
            formula: this.parseFormula(),
        }
    }

    parseFormula(): Formula {
        const formula = this.parseImplication()

        if (!this.tryConsumeToken('iff'))
            return formula

        const formula2 = this.parseFormula()

        return new Formula.Conjunction([
            new Formula.Implication([formula, formula2]),
            new Formula.Implication([formula2, formula]),
        ])
    }

    parseImplication(): Formula {
        const formula = this.parseDisjunction()

        return this.tryConsumeToken('implies')
            ? new Formula.Implication([formula, this.parseImplication()])
            : formula
    }

    parseDisjunction(): Formula {
        const formula = this.parseConjunction()

        return this.tryConsumeToken('or')
            ? new Formula.Disjunction([formula, this.parseDisjunction()])
            : formula
    }

    parseConjunction(): Formula {
        const formula = this.parseFactor()

        return this.tryConsumeToken('&')
            ? new Formula.Conjunction([formula, this.parseConjunction()])
            : formula
    }

    parseFactor(): Formula {
        switch (this.token.type) {
        case 'for':
            return this.parseForQuantor()

        case 'ex':
            return this.parseExQuantor()

        case 'not':
            this.nextToken()
            return new Formula.Implication([this.parseFactor(), Formula.False])

        case '(': {
            const {index} = this.token
            let formula: Formula

            try {
                this.nextToken()
                formula = this.parseFormula()
            } catch (error) {
                if (!(error instanceof ClassSyntaxError))
                    throw error

                try {
                    this.tokens.setSourceIndex(index)
                    this.nextToken()
                    return this.parseAtom()
                } catch (error_) {
                    throw error_ instanceof ClassSyntaxError && error.token.index > error_.token.index
                        ? error
                        : error_
                }
            }

            this.consumeToken(')')
            return formula
        }

        case 'true':
            this.nextToken()
            return Formula.True

        case 'false':
            this.nextToken()
            return Formula.False

        case 'thesis': {
            this.nextToken()

            let formula = this.reasoner.thesis

            if (!formula) {
                this.logError('"thesis" not allowed here')
                formula = Formula.True
            }

            return formula
        }

        default:
            return this.parseAtom()
        }
    }

    parseForQuantor() {
        this.consumeToken('for')

        const variables = pipe(
            this.parseList(this.parseQualifiedVariable),
            map(varSpec => new QuantifiedVariableTerm(varSpec)),
            tap(variable => this.verifier.addBoundVariable(variable)),
            toArray,
        )

        let formula = this.tryConsumeToken('st') && this.parseFormula()

        if (this.token.type !== 'ex')
            this.consumeToken('holds')

        formula = formula
            ? new Formula.Implication([formula, this.parseFormula()])
            : this.parseFormula()

        for (const variable of reverse(variables)) {
            formula = new Formula.Generalization(variable, formula)
            this.verifier.removeBoundVariable()
        }

        return formula
    }

    parseExQuantor() {
        this.consumeToken('ex')

        const variables = pipe(
            this.parseList(this.parseQualifiedVariable),
            map(varSpec => new QuantifiedVariableTerm(varSpec)),
            tap(variable => this.verifier.addBoundVariable(variable)),
            toArray,
        )

        this.consumeToken('st')

        let formula = this.parseFormula()

        for (const variable of reverse(variables)) {
            formula = new Formula.Existence(variable, formula)
            this.verifier.removeBoundVariable()
        }

        return formula
    }

    parseQualifiedVariable(): VariableSpecification {
        const name = this.token.string

        this.consumeToken('_identifier_')

        let type = this.tryConsumeToken('be')
            ? this.parseType()
            : this.verifier.getReservedType(name)

        if (!type) {
            this.logError(`unknown type of variable "${name}"`)
            type = Verifier.defaultType
        }

        return {name, type}
    }

    parseAtom() {
        if (this.symbols[this.token.string]?.kind === 'relation')
            return this.parsePredicate()

        const parameters = [...this.parseList(this.parseTerm)]

        if (parameters.length == 1 && this.tryConsumeToken('is'))
            return new Formula.TypeAssertion(parameters[0], this.parseType())

        if (parameters.length == 1 && this.tryConsumeToken('=')) {
            parameters.push(this.parseTerm())
            const types = parameters.map(parameter => parameter.getType())

            if (!isSubtypeOf(types[0], types[1]) && !isSubtypeOf(types[1], types[0]))
                this.logError(`"${types[0].name}" and "${types[1].name}" types not related`)

            return new Formula.Equality(parameters[0], parameters[1])
        }

        return this.parsePredicate(parameters)
    }

    parsePredicate(parameters: Term[] = []) {
        const symbolToken = this.token
        const name = symbolToken.string
        const specifications = this.predicateSpecifications[name]
        const symbolOffset = parameters.length

        if (!specifications)
            throw this.error(`predicate symbol expected but "${name}" found`, this.token)

        this.consumeToken('_symbol_')

        if (this.isTermLike())
            parameters.push(...this.parseList(this.parseTerm))

        const specification = specifications
            .find(
                specification =>
                    specification.symbolOffset == symbolOffset &&
                    parameters.length == specification.parameterTypes.length &&
                    pipe(
                        zip(parameters, specification.parameterTypes),
                        every(([parameter, type]) => isSubtypeOf(parameter.getType(), type)),
                    ),
            )

        if (!specification) {
            const wantedSpecification = {
                name,
                symbolOffset,
                parameterTypes: parameters.map(parameter => parameter.getType()),
            }

            this.logError(
                `no specification "${stringifyPredicateSpecification(wantedSpecification)}" found`,
                symbolToken,
            )

            return Formula.True
        }

        return new Formula.Predicate(specification, parameters)
    }

    isTermLike(token = this.token) {
        return ['_identifier_', '(', '_symbol_'].includes(token.type)
    }

    parseTerm(): Term {
        const terms = this.parseOperationTerm(this.operationPrecedences.length - 1)

        if (terms.length != 1)
            throw this.error('term syntax error')

        return terms[0]
    }

    parseOperationTerm(precedence: number): Term[] {
        if (precedence < 0)
            return this.parseTermFactor()

        let parameters: Term[] = this.operationPrecedences[precedence].includes(this.token.string)
            ? []
            : [...this.parseOperationTerm(precedence - 1)]

        while (this.operationPrecedences[precedence].includes(this.token.string)) {
            const nameToken = this.token
            const name = nameToken.string
            const offset = parameters.length

            this.nextToken()

            if (this.isTermFactorLike(precedence - 1))
                parameters.push(...this.parseOperationTerm(precedence - 1))

            const specification = this.getOperationSpecification(name, parameters, offset)

            if (specification)
                parameters = [new FunctionTerm(
                    specification,
                    parameters,
                )]
            else {
                const wantedSpecification = {
                    name,
                    symbolOffset: offset,
                    parameterTypes: parameters.map(parameter => parameter.getType()),
                    type: Verifier.defaultType,
                }

                this.logError(
                    `no specification "${stringifyFunctionSpecification(wantedSpecification)}" found`,
                    nameToken,
                )

                parameters = [Verifier.defaultVariable]
            }
        }

        return parameters
    }

    isTermFactorLike(precedence: number, token = this.token) {
        return token.type === '_identifier_' ||
            token.type === '(' ||
            this.symbols[token.string]?.kind === 'leftBracket' ||
            pipe(
                this.operationPrecedences,
                take(precedence + 1),
                flat<string>,
                includes(token.string),
            )
    }

    parseTermFactor(): Term[] {
        if (this.token.type === '_identifier_') {
            const name = this.token.string
            const variable = this.verifier.resolveVariable(name)

            if (!variable)
                this.logError(`unknown variable "${name}"`, this.token)

            this.nextToken()

            return [variable || Verifier.defaultVariable]
        }

        if (this.symbols[this.token.string]?.kind === 'leftBracket')
            return [this.parseBracketTerm()]

        if (this.tryConsumeToken('(')) {
            const terms = [...this.parseList(this.parseTerm)]
            this.consumeToken(')')

            return terms
        }

        throw this.error('syntax error', this.token)
    }

    parseBracketTerm(): Term {
        const leftBracketToken = this.token
        const symbol = this.symbols[leftBracketToken.string]

        if (symbol?.kind !== 'leftBracket')
            throw this.error(`bracket function expected but "${this.token.string}" found`, this.token)

        this.consumeToken('_symbol_')

        const parameters = [...this.parseList(this.parseTerm)]

        if (this.token.string !== symbol.pair)
            throw this.error(`"${symbol.pair}" expected but "${this.token.string}" found`, this.token)

        this.consumeToken('_symbol_')

        const specification = this.getOperationSpecification(leftBracketToken.string, parameters)

        if (!specification) {
            const wantedSpecification = {
                left: leftBracketToken.string,
                right: symbol.pair,
                parameterTypes: parameters.map(parameter => parameter.getType()),
                type: Verifier.defaultType,
            }

            this.logError(
                `no specification "${stringifyFunctionSpecification(wantedSpecification)}" found`,
                leftBracketToken,
            )

            return Verifier.defaultVariable
        }

        return new FunctionTerm(
            specification,
            parameters,
        )
    }

    getOperationSpecification(symbol: string, parameters: Term[], symbolOffset?: number) {
        return (this.functionSpecifications[symbol] || [])
            .find(
                specification =>
                    parameters.length == specification.parameterTypes.length &&
                    symbolOffset === ('symbolOffset' in specification ? specification.symbolOffset : undefined) &&
                    pipe(
                        zip(parameters, specification.parameterTypes),
                        every(([parameter, type]) => isSubtypeOf(parameter.getType(), type)),
                    ),
            )
    }

    addSymbol(name: string, symbolInfo: SymbolInfo) {
        if (this.symbols[name])
            this.logError(`duplicate symbol "${name}"`)
        else {
            this.tokens.addSymbol(name)
            this.symbols[name] = symbolInfo
        }
    }

    consumeToken(token: TokenType) {
        if (!this.tryConsumeToken(token))
            throw this.error(`"${token}" expected but "${this.token.string}" found`, this.token)
    }

    tryConsumeToken(token: TokenType) {
        if (this.token.type !== token)
            return false

        return this.nextToken()
    }

    nextToken() {
        this.previousToken = this.token

        do
            this.token = this.nextLooseToken()
        while (['_space_', '_comment_'].includes(this.token.type))

        return this.token
    }

    nextLooseToken() {
        this.token = this.peekedToken || this.tokens.next().value
        this.peekedToken = undefined
        return this.token
    }

    peekToken() {
        return this.peekedToken ||= this.tokens.next().value
    }
}
